$\forall$$T$:Type, $L$:($T$ List). ($\neg$($\uparrow$null($L$))) $\Rightarrow$ ($\exists$${\it L'}$:$T$ List. ($L$ = append(${\it L'}$; cons(last($L$); []))))